$\forall$$x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Top, ${\it da}$:$a$:Knd fp$\rightarrow$ Top, $f$:Top, $l$:IdLnk, ${\it tg}$:Id, $L$:Top.
\\[0ex]with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v $\Vert\!+$ only $L$ sends on ($l$ with ${\it tg}$)